| 翻訳と辞書 |
| Finite model property ： ウィキペディア英語版 |
Finite model property
In logic, we say a logic L has the finite model property (fmp for short) if there is a class of models M of L (i.e. each model in M is a model of L) such that any non-theorem of L is falsified by some ''finite'' model in M. Another way of putting this is to say that L has the fmp if for every formula A of L, A is an L-theorem iff A is a theorem of the theory of finite models of L.
If L is finitely axiomatizable (and has a recursive set of recursive rules) and has the fmp, then it is decidable. However, the strengthened claim that if L is recursively axiomatizable and the fmp then it is decidable, is false. Even if there are only finitely many finite models to choose from (up to isomorphism) there is still the problem of checking whether the underlying frames of such models validate the logic, and this may not be decidable when the logic is not finitely axiomatizable, even when it is recursively axiomatizable. (Note that a logic is recursively enumerable iff it is recursively axiomatizable, a result known as Craig's theorem.)
== Example ==
A first-order formula with one universal quantification has the fmp. A first-order formula without functional symbols, where all existential quantifications appear first in the formula, also has the fmp.〔Leonid Libkin, ''Elements of finite model theory'', chapter 14〕
抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』
■ウィキペディアで「Finite model property」の詳細全文を読む
スポンサード リンク
| 翻訳と辞書 : 翻訳のためのインターネットリソース |
Copyright(C) kotoba.ne.jp 1997-2016. All Rights Reserved.
|
|